Constraint Logic Programming (CLP) and Hereditary Harrop formulas (HH) aretwo well known ways to enhance the expressivity of Horn clauses. In this paper,we present a novel combination of these two approaches. We show how to enrichthe syntax and proof theory of HH with the help of a given constraint system,in such a way that the key property of HH as a logic programming language(namely, the existence of uniform proofs) is preserved. We also present aprocedure for goal solving, showing its soundness and completeness forcomputing answer constraints. As a consequence of this result, we obtain a newstrong completeness theorem for CLP that avoids the need to build disjunctionsof computed answers, as well as a more abstract formulation of a knowncompleteness theorem for HH.
展开▼
